as:Top List, f:Top. null(as)  (last(map(f;as)) ~ (f(last(as)))) 

latex

Definitions	t  T, Top, x:A. B(x), ||as||, AB, P & Q, i  j < k, P  Q, False, A, {i..j}, last(L), null(as), b, ij, Prop, P  Q
Lemmas	not functionality wrt iff, assert of null, pos length, not wf, assert wf, null wf3, length-map, select-map, le wf, length wf1, top wf